$\vdash$  $\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $p$:($a$:$A$ $\times$ $B$($a$)). ($p$.2) $\in$ $B$($p$.1)